Метод распространения переменной

КНФ $F$ с клозами $C_{1}, \dots, C_{\ell}$ и переменными $x_{1}, \dots, x_{n}$ представляется двумя массивами: $L[1 \dots 2n]$ — $L[i]$ хранит номера клозов, куда входит литерал $x_{i}$ (при $i \le n$) или $\bar{x}_{i-n}$ (при $i > n$). $C[1 \dots \ell]$ — $C[i]$ хранит номера литералов, входящих в клоз $C_{i}$. При подготовке КНФ клозы, содержащие одновременно $x_{i}$ и $\bar{x}_{i}$, удаляются.

**Распространение переменной** — процедура упрощения КНФ $F$, основанная на единичных клозах. Если в $F$ есть клоз из одного литерала ($x_{i}$ или $\bar{x}_{i}$), то значение переменной для выполнения $F$ определяется однозначно. Алгоритм: 1. Выбрать значение $b_{i}$, выполняющее данный клоз. 2. Удалить все клозы, содержащие этот литерал (они выполнены). 3. Из клозов, содержащих противоположный литерал, удалить этот литерал. 4. Если при удалении литерала образовался новый единичный клоз, добавить его в очередь на обработку. Процедура выполняется в цикле, пока очередь не опустеет. Если в процессе возник пустой клоз, то КНФ $F$ невыполнима.

Пусть $UP(F)$ — результат работы процедуры распространения переменной. Справедливо следующее: $UP(F) = 1$, если в итоге удалены все клозы. $UP(F) = 0$, если встретился пустой клоз. $UP(F)$ выполнима $\iff F$ выполнима. Сложность: Распространение переменной выполняется за время $O(N)$, где $N$ — суммарное число вхождений литералов в формулу $F$.